\begin{tabbing}
$\forall$\=$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $f$:fpf($A$; $x$.$B$($x$)),\+
\\[0ex]$P$:($x$:\{$x$:$A$$\mid$ $\uparrow$fpf{-}dom(${\it eq}$; $x$; $f$)\} $\rightarrow$$B$($x$)$\rightarrow$prop\{i:l\}).
\-\\[0ex]fpf{-}all($A$; ${\it eq}$; $f$; $x$,$v$.$P$($x$,$v$)) $\in$ prop\{i:l\}
\end{tabbing}